\begin{tabbing}
single{-}thread{-}generator\=\{i:l\}\+
\\[0ex](${\it es}$; $P$; $R$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$e$:es{-}E(${\it es}$). Dec($P$($e$)))\+
\\[0ex]\& ($\forall$$e$:es{-}E(${\it es}$), ${\it e'}$:es{-}E(${\it es}$). Dec($R$(${\it e'}$,$e$)))
\\[0ex]\& rel\_implies(es{-}E(${\it es}$);$R$;$\lambda$$x$,$y$. es{-}causl(${\it es}$; $x$; $y$))
\\[0ex]\& ($\forall$$e$:es{-}E(${\it es}$), ${\it e'}$:es{-}E(${\it es}$). ($P$($e$) \& $R$(${\it e'}$,$e$)) $\Rightarrow$ $P$(${\it e'}$))
\\[0ex]\& (\=$\forall$$m$:es{-}E(${\it es}$), ${\it m'}$:es{-}E(${\it es}$).\+
\\[0ex]$P$($m$)
\\[0ex]$\Rightarrow$ $P$(${\it m'}$)
\\[0ex]$\Rightarrow$ ($\forall$$e$:es{-}E(${\it es}$). ($e$ $R$ $m$) $\Rightarrow$ ($\neg$$P$($e$)))
\\[0ex]$\Rightarrow$ ($\forall$$e$:es{-}E(${\it es}$). ($e$ $R$ ${\it m'}$) $\Rightarrow$ ($\neg$$P$($e$)))
\\[0ex]$\Rightarrow$ ($m$ = ${\it m'}$ $\in$ es{-}E(${\it es}$)))
\-\\[0ex]\& (\=$\forall$$a$:es{-}E(${\it es}$).\+
\\[0ex]$\forall$$b$:es{-}E(${\it es}$), $e$:es{-}E(${\it es}$).
\\[0ex]($R$($e$,$a$) \& $R$($e$,$b$)) $\Rightarrow$ ($P$($e$) \& $P$($a$) \& $P$($b$)) $\Rightarrow$ ($a$ = $b$ $\in$ es{-}E(${\it es}$)))
\-\-
\end{tabbing}